Nuprl Lemma : uni_sat_imp_in_uni_set
9,38
postcript
pdf
T
:Type,
a
:
T
,
Q
:(
T
). (
a
= !
x
:
T
.
Q
(
x
))
(
a
{!
x
:
T
|
Q
(
x
)})
latex
ProofTree
Definitions
P
Q
,
{!
x
:
T
|
P
(
x
)}
,
t
T
,
x
(
s
)
,
a
= !
x
:
T
.
Q
(
x
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
origin
T:Type, a:T, Q:(T
). (a = !x:T. Q(x)) 
(a 
{!x:T | Q(x)})
T:Type, a:T, Q:(T). (a = !x:T. Q(x)) (a {!x:T | Q(x)})
Q T Qx:A. B(x)